'Weak Dependency Graph [60.0]' ------------------------------ Answer: YES(?,O(n^1)) Input Problem: innermost runtime-complexity with respect to Rules: { f(f(X)) -> f(a(b(f(X)))) , f(a(g(X))) -> b(X) , b(X) -> a(X)} Details: We have computed the following set of weak (innermost) dependency pairs: { f^#(f(X)) -> c_0(f^#(a(b(f(X))))) , f^#(a(g(X))) -> c_1(b^#(X)) , b^#(X) -> c_2()} The usable rules are: { f(f(X)) -> f(a(b(f(X)))) , f(a(g(X))) -> b(X) , b(X) -> a(X)} The estimated dependency graph contains the following edges: {f^#(f(X)) -> c_0(f^#(a(b(f(X)))))} ==> {f^#(a(g(X))) -> c_1(b^#(X))} {f^#(a(g(X))) -> c_1(b^#(X))} ==> {b^#(X) -> c_2()} We consider the following path(s): 1) { f^#(f(X)) -> c_0(f^#(a(b(f(X))))) , f^#(a(g(X))) -> c_1(b^#(X)) , b^#(X) -> c_2()} The usable rules for this path are the following: { f(f(X)) -> f(a(b(f(X)))) , f(a(g(X))) -> b(X) , b(X) -> a(X)} We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs. 'Weight Gap Principle' ---------------------- Answer: YES(?,O(n^1)) Input Problem: innermost runtime-complexity with respect to Rules: { f(f(X)) -> f(a(b(f(X)))) , f(a(g(X))) -> b(X) , b(X) -> a(X) , f^#(a(g(X))) -> c_1(b^#(X)) , f^#(f(X)) -> c_0(f^#(a(b(f(X))))) , b^#(X) -> c_2()} Details: We apply the weight gap principle, strictly orienting the rules {f^#(a(g(X))) -> c_1(b^#(X))} and weakly orienting the rules {} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {f^#(a(g(X))) -> c_1(b^#(X))} Details: Interpretation Functions: f(x1) = [1] x1 + [0] a(x1) = [1] x1 + [0] b(x1) = [1] x1 + [0] g(x1) = [1] x1 + [0] f^#(x1) = [1] x1 + [1] c_0(x1) = [1] x1 + [7] c_1(x1) = [1] x1 + [0] b^#(x1) = [1] x1 + [0] c_2() = [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {b^#(X) -> c_2()} and weakly orienting the rules {f^#(a(g(X))) -> c_1(b^#(X))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {b^#(X) -> c_2()} Details: Interpretation Functions: f(x1) = [1] x1 + [0] a(x1) = [1] x1 + [0] b(x1) = [1] x1 + [0] g(x1) = [1] x1 + [0] f^#(x1) = [1] x1 + [1] c_0(x1) = [1] x1 + [0] c_1(x1) = [1] x1 + [0] b^#(x1) = [1] x1 + [1] c_2() = [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {f(a(g(X))) -> b(X)} and weakly orienting the rules { b^#(X) -> c_2() , f^#(a(g(X))) -> c_1(b^#(X))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {f(a(g(X))) -> b(X)} Details: Interpretation Functions: f(x1) = [1] x1 + [0] a(x1) = [1] x1 + [0] b(x1) = [1] x1 + [0] g(x1) = [1] x1 + [2] f^#(x1) = [1] x1 + [0] c_0(x1) = [1] x1 + [0] c_1(x1) = [1] x1 + [2] b^#(x1) = [1] x1 + [0] c_2() = [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {b(X) -> a(X)} and weakly orienting the rules { f(a(g(X))) -> b(X) , b^#(X) -> c_2() , f^#(a(g(X))) -> c_1(b^#(X))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {b(X) -> a(X)} Details: Interpretation Functions: f(x1) = [1] x1 + [0] a(x1) = [1] x1 + [4] b(x1) = [1] x1 + [8] g(x1) = [1] x1 + [7] f^#(x1) = [1] x1 + [0] c_0(x1) = [1] x1 + [0] c_1(x1) = [1] x1 + [3] b^#(x1) = [1] x1 + [2] c_2() = [0] Finally we apply the subprocessor 'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment'' ------------------------------------------------------------------------------------------ Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { f(f(X)) -> f(a(b(f(X)))) , f^#(f(X)) -> c_0(f^#(a(b(f(X)))))} Weak Rules: { b(X) -> a(X) , f(a(g(X))) -> b(X) , b^#(X) -> c_2() , f^#(a(g(X))) -> c_1(b^#(X))} Details: The problem was solved by processor 'Bounds with default enrichment': 'Bounds with default enrichment' -------------------------------- Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { f(f(X)) -> f(a(b(f(X)))) , f^#(f(X)) -> c_0(f^#(a(b(f(X)))))} Weak Rules: { b(X) -> a(X) , f(a(g(X))) -> b(X) , b^#(X) -> c_2() , f^#(a(g(X))) -> c_1(b^#(X))} Details: The problem is Match-bounded by 0. The enriched problem is compatible with the following automaton: { a_0(2) -> 2 , a_0(4) -> 2 , g_0(2) -> 4 , g_0(4) -> 4 , f^#_0(2) -> 5 , f^#_0(4) -> 5 , c_1_0(8) -> 5 , b^#_0(2) -> 8 , b^#_0(4) -> 8 , c_2_0() -> 8} 2) { f^#(f(X)) -> c_0(f^#(a(b(f(X))))) , f^#(a(g(X))) -> c_1(b^#(X))} The usable rules for this path are the following: { f(f(X)) -> f(a(b(f(X)))) , f(a(g(X))) -> b(X) , b(X) -> a(X)} We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs. 'Weight Gap Principle' ---------------------- Answer: YES(?,O(n^1)) Input Problem: innermost runtime-complexity with respect to Rules: { f(f(X)) -> f(a(b(f(X)))) , f(a(g(X))) -> b(X) , b(X) -> a(X) , f^#(f(X)) -> c_0(f^#(a(b(f(X))))) , f^#(a(g(X))) -> c_1(b^#(X))} Details: We apply the weight gap principle, strictly orienting the rules {f^#(a(g(X))) -> c_1(b^#(X))} and weakly orienting the rules {} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {f^#(a(g(X))) -> c_1(b^#(X))} Details: Interpretation Functions: f(x1) = [1] x1 + [0] a(x1) = [1] x1 + [0] b(x1) = [1] x1 + [0] g(x1) = [1] x1 + [0] f^#(x1) = [1] x1 + [1] c_0(x1) = [1] x1 + [0] c_1(x1) = [1] x1 + [0] b^#(x1) = [1] x1 + [0] c_2() = [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {f(a(g(X))) -> b(X)} and weakly orienting the rules {f^#(a(g(X))) -> c_1(b^#(X))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {f(a(g(X))) -> b(X)} Details: Interpretation Functions: f(x1) = [1] x1 + [0] a(x1) = [1] x1 + [0] b(x1) = [1] x1 + [0] g(x1) = [1] x1 + [1] f^#(x1) = [1] x1 + [0] c_0(x1) = [1] x1 + [0] c_1(x1) = [1] x1 + [1] b^#(x1) = [1] x1 + [0] c_2() = [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {b(X) -> a(X)} and weakly orienting the rules { f(a(g(X))) -> b(X) , f^#(a(g(X))) -> c_1(b^#(X))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {b(X) -> a(X)} Details: Interpretation Functions: f(x1) = [1] x1 + [0] a(x1) = [1] x1 + [0] b(x1) = [1] x1 + [8] g(x1) = [1] x1 + [12] f^#(x1) = [1] x1 + [0] c_0(x1) = [1] x1 + [2] c_1(x1) = [1] x1 + [3] b^#(x1) = [1] x1 + [1] c_2() = [0] Finally we apply the subprocessor 'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment'' ------------------------------------------------------------------------------------------ Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { f(f(X)) -> f(a(b(f(X)))) , f^#(f(X)) -> c_0(f^#(a(b(f(X)))))} Weak Rules: { b(X) -> a(X) , f(a(g(X))) -> b(X) , f^#(a(g(X))) -> c_1(b^#(X))} Details: The problem was solved by processor 'Bounds with default enrichment': 'Bounds with default enrichment' -------------------------------- Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { f(f(X)) -> f(a(b(f(X)))) , f^#(f(X)) -> c_0(f^#(a(b(f(X)))))} Weak Rules: { b(X) -> a(X) , f(a(g(X))) -> b(X) , f^#(a(g(X))) -> c_1(b^#(X))} Details: The problem is Match-bounded by 0. The enriched problem is compatible with the following automaton: { a_0(2) -> 2 , a_0(4) -> 2 , g_0(2) -> 4 , g_0(4) -> 4 , f^#_0(2) -> 5 , f^#_0(4) -> 5 , c_1_0(8) -> 5 , b^#_0(2) -> 8 , b^#_0(4) -> 8} 3) {f^#(f(X)) -> c_0(f^#(a(b(f(X)))))} The usable rules for this path are the following: { f(f(X)) -> f(a(b(f(X)))) , f(a(g(X))) -> b(X) , b(X) -> a(X)} We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs. 'Weight Gap Principle' ---------------------- Answer: YES(?,O(n^1)) Input Problem: innermost runtime-complexity with respect to Rules: { f(f(X)) -> f(a(b(f(X)))) , f(a(g(X))) -> b(X) , b(X) -> a(X) , f^#(f(X)) -> c_0(f^#(a(b(f(X)))))} Details: We apply the weight gap principle, strictly orienting the rules {f(a(g(X))) -> b(X)} and weakly orienting the rules {} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {f(a(g(X))) -> b(X)} Details: Interpretation Functions: f(x1) = [1] x1 + [0] a(x1) = [1] x1 + [0] b(x1) = [1] x1 + [0] g(x1) = [1] x1 + [4] f^#(x1) = [1] x1 + [0] c_0(x1) = [1] x1 + [4] c_1(x1) = [0] x1 + [0] b^#(x1) = [0] x1 + [0] c_2() = [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {b(X) -> a(X)} and weakly orienting the rules {f(a(g(X))) -> b(X)} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {b(X) -> a(X)} Details: Interpretation Functions: f(x1) = [1] x1 + [0] a(x1) = [1] x1 + [0] b(x1) = [1] x1 + [8] g(x1) = [1] x1 + [12] f^#(x1) = [1] x1 + [8] c_0(x1) = [1] x1 + [0] c_1(x1) = [0] x1 + [0] b^#(x1) = [0] x1 + [0] c_2() = [0] Finally we apply the subprocessor 'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment'' ------------------------------------------------------------------------------------------ Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { f(f(X)) -> f(a(b(f(X)))) , f^#(f(X)) -> c_0(f^#(a(b(f(X)))))} Weak Rules: { b(X) -> a(X) , f(a(g(X))) -> b(X)} Details: The problem was solved by processor 'Bounds with default enrichment': 'Bounds with default enrichment' -------------------------------- Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { f(f(X)) -> f(a(b(f(X)))) , f^#(f(X)) -> c_0(f^#(a(b(f(X)))))} Weak Rules: { b(X) -> a(X) , f(a(g(X))) -> b(X)} Details: The problem is Match-bounded by 0. The enriched problem is compatible with the following automaton: { a_0(2) -> 2 , a_0(4) -> 2 , g_0(2) -> 4 , g_0(4) -> 4 , f^#_0(2) -> 5 , f^#_0(4) -> 5}